Metamath Blueprint : Derivative of real logarithm (iset)

Theorem dvrelog

StmtFormalized
https://us.metamath.org/mpeuni/dvrelog.html

The derivative of the real logarithm function

The derivative of the logarithm is the reciprocal:

( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )